(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun aa () Real)
(declare-fun e () Real)
(assert (not (exists ((f Real)) (= (=> (<= 0.0 f b) (<= 0.0 (+ (/ (* (- a aa)) f (* (div a aa)) f)) d)) (distinct e 2.0)))))
(assert (= a (+ c aa)))
(check-sat)
